In the first part of the video, we review the basic functionalities we need in order to write formulas and manipulate the solver.

To write a boolean formula, we will need to declare boolean variables for the solver. You can do this in Python using the Bool() constructor. For example, we can start by creating two boolean variables x and y:

>>> from z3 import * >>> x = Bool("x") >>> y = Bool("y")

With boolean variables, you can build boolean formulas. z3 gives you constructors for disjunctions and conjunctions, negation, and equivalence:

>>> x_or_y = Or([x,y]) # disjunction >>> x_and_y = And([x,y]) # conjunction >>> not_x = Not(x) # negation >>> x_or_y_iff_not_x = x_and_y == not_x # This is the formula (x_or_y not_x) not a boolean!

Once we have built the clauses that compose our problem, we can pass them to a solver:

>>> s = Solver() # create a solver s >>> s.add(x_or_y) # add the clause: x or y >>> z = Bool("z") >>> s.add(Or[x,y,Not(z)]) # add another clause: x or y or !z

Calling s.check() at that point will ask the solver to find a satisfying assignment for the boolean formula built from the conjunction of all the clauses that have been added through s.add(..). In our running example, the call should return sat:

>>> s.check() sat

If the solver cannot find a satisfying assignment, then it will return unsat. In the case it returned sat, you can obtain the assignment itself with the model() method:

>>> s.model() [x = False, y = True, z = False]

And that is all you need for this tutorial, as well as for the assignment. The difficulty will be to design the encoding, not to use the solver!